↳ Prolog
↳ PrologToPiTRSProof
log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)
LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)
log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)
log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)
log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
LOG2_IN(X, s(s(Half)), Acc) → U31(Half, Acc, small_in(X))
LOG2_IN(s(s(X)), Half, Acc) → LOG2_IN(X, s(Half), Acc)
U31(Half, Acc, small_out) → LOG2_IN(Half, s(0), s(Acc))
small_in(s(0)) → small_out
small_in(0) → small_out
small_in(x0)
LOG2_IN(X, s(s(Half)), Acc) → U31(Half, Acc, small_in(X))
LOG2_IN(s(s(X)), Half, Acc) → LOG2_IN(X, s(Half), Acc)
small_in(s(0)) → small_out
POL(0) = 1
POL(LOG2_IN(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U31(x1, x2, x3)) = 1 + 2·x1 + x2 + 2·x3
POL(s(x1)) = 1 + x1
POL(small_in(x1)) = 1 + x1
POL(small_out) = 2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
U31(Half, Acc, small_out) → LOG2_IN(Half, s(0), s(Acc))
small_in(0) → small_out
small_in(x0)